Nuprl Lemma : scheme-none_wf
11,40
postcript
pdf
scheme-none()
RealizerScheme{i:l}()
latex
Definitions
Rnone()
,
t
T
,
x
:
A
.
B
(
x
)
,
scheme-constant(
R
)
,
scheme-none()
Lemmas
scheme-constant
wf
,
Rnone
wf
origin
RealizerScheme{i:l}() RealizerScheme{i:l}() T
x:A. B(x)